


\begin{figure}
\begin{center}
\begin{minipage}{0.5\textwidth}
\begin{tikzpicture}[font=\small,framed, node distance=3.4cm, 
%state/.style={circle, draw=blue!50,fill=blue!10,thick, minimum size = 13mm}
state/.style={circle,thick,draw=red!80, fill=gray!40,minimum size=5mm}
]


\node [state] (before)        {};
\node [yshift=2mm] at (before.north) {t0\_before};
%\node (beforeandpoll) [yshift=-5mm] at (before.south) {};
%
\node [state] (poll)   [right of=before]    {};
\node [yshift=2mm] at (poll.north) {t0\_poll};
%\node (belowofpoll) [below of=poll] {};
%\node (pollandafter) [yshift=-6.5mm] at (belowofpoll.south) {};
%
\node [state] (after)  [right of=poll]      {};
\node [yshift=2mm] at (after.north) {t0\_after};

\path[->, very thick]  (before) edge node [below]  {\textrm{++g\_mutex}} (poll) 
                       (poll) edge node [below]  {\textrm{g\_mutex==goalVal}} (after) ;
\end{tikzpicture}
\end{minipage}
\end{center}
\caption{Model of the simple barrier in Fig. \ref{code:cs}. Initially, all leading threads are in state ``t0\_before''.}
\label{model:cs}
\end{figure}
